On the categorical semantics of dependent type theory with function types in locally cartesian closed categories (see at relation between category theory and type theory):
Pierre-Louis Curien, Substitution up to isomorphism, Fundamenta Informaticae, 19 1-2 (1993) 51-86 [doi:10.5555/175469.175471] and: Diagrammes 23 (1990) 43-66 [numdam:DIA_1990__23__43_0]
Pierre-Louis Curien, Richard Garner, Martin Hofmann, Revisiting the categorical interpretation of dependent type theory, Theoretical Computer Science 546 21 (2014) 99-119 [doi:10.1016/j.tcs.2014.03.003, pdf]
Last revised on January 22, 2023 at 16:16:05. See the history of this page for a list of all contributions to it.